$\forall$${\it es}$:event\_system\{i:l\}, $i$:Id, ${\it ds}$:fpf(Id; $x$.Type), ${\it da}$:fpf(Knd; $k$.Type). \\[0ex]es{-}decls(${\it es}$;$i$;${\it ds}$;${\it da}$) $\in$ prop\{i:l\}